es:event_system{i:l}, e:es-E(es), x:Id, T:Type.
es-dtype(es; loc(e); x; T)
 (t:rationals. es-state-after-elapsed(es; e; t)(x) = es-after(es; x; e)  T) 

latex

Definitions

P  Q, es-dtype(es; i; x; T), quotient(A; x,y.B(x;y)), rationals, s = t, f(a), es-vartype(es; i; x), x:AB(x), t  T, x:A  B(x), event_system{i:l}, t.1, es-E(es), atom{$n:n}, Id, Type, b, es_vartype(es; i; x), es_state(es; i), es-T(es), x:A. B(x), P  Q, es_state_after(es; e), es-state-after-elapsed(es; e; t), prop{i:l}, es-state(es; i), <a, b>, sqequal(s; t), guard(T), sq_type(T), es-state-ap(s; x), loc(e), es-after(es; x; e), #$n

Lemmas

rationals wf, es-dtype wf, es-loc wf, Id wf, es-E wf, event system wf, es-isconst-property, int-rational, es state after wf, es state wf, es-state-after-elapsed wf, subtype rel wf, es-vartype wf